A, B:Type, R:(AA), S:(BB), f:(AB).
RelsIso(A;B;x,y.R(x,y);x,y.S(x,y);f)  Connex(B;x,y.S(x,y))  Connex(A;x,y.R(x,y)) 

latex

Up	gen algebra 1
Definitions of Statement	RelsIso(T;T';x,y.R(x;y);x,y.R'(x;y);f)
Definitions	x,y. t(x;y), t  T, Connex(T;x,y.R(x;y)), x(s1,s2), P  Q, , x:A. B(x), RelsIso(T;T';x,y.R(x;y);x,y.R'(x;y);f), P & Q, P  Q, P  Q
Lemmas	rels iso wf, connex wf, or functionality wrt iff